home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / prolog / prlgbnc1.lha / Bench / boyer.pl next >
Text File  |  1990-07-13  |  11KB  |  388 lines
  1. % generated: 20 November 1989
  2. % option(s): 
  3. %
  4. %   boyer
  5. %
  6. %   Evan Tick (from Lisp version by R. P. Gabriel)
  7. %
  8. %   November 1985
  9. %
  10. %   prove arithmetic theorem
  11.  
  12. main :- wff(Wff),
  13.     rewrite(Wff,NewWff),
  14.     tautology(NewWff,[],[]).
  15.  
  16. wff(implies(and(implies(X,Y),
  17.                 and(implies(Y,Z),
  18.                     and(implies(Z,U),
  19.                         implies(U,W)))),
  20.             implies(X,W))) :-
  21.         X = f(plus(plus(a,b),plus(c,zero))),
  22.         Y = f(times(times(a,b),plus(c,d))),
  23.         Z = f(reverse(append(append(a,b),[]))),
  24.         U = equal(plus(a,b),difference(x,y)),
  25.         W = lessp(remainder(a,b),member(a,length(b))).
  26.  
  27. tautology(Wff) :-
  28.         write('rewriting...'),nl,
  29.         rewrite(Wff,NewWff),
  30.         write('proving...'),nl,
  31.         tautology(NewWff,[],[]).
  32.  
  33. tautology(Wff,Tlist,Flist) :-
  34.         (truep(Wff,Tlist) -> true
  35.         ;falsep(Wff,Flist) -> fail
  36.         ;Wff = if(If,Then,Else) ->
  37.         (truep(If,Tlist) -> tautology(Then,Tlist,Flist)
  38.         ;falsep(If,Flist) -> tautology(Else,Tlist,Flist)
  39.         ;tautology(Then,[If|Tlist],Flist),    % both must hold
  40.          tautology(Else,Tlist,[If|Flist])
  41.                 )
  42.         ),!.
  43.  
  44. rewrite(Atom,Atom) :-
  45.         atomic(Atom),!.
  46. rewrite(Old,New) :-
  47.         functor(Old,F,N),
  48.         functor(Mid,F,N),
  49.         rewrite_args(N,Old,Mid),
  50.         ( equal(Mid,Next),        % should be ->, but is compiler smart
  51.           rewrite(Next,New)       % enough to generate cut for -> ?
  52.         ; New=Mid
  53.         ),!.
  54.  
  55. rewrite_args(0,_,_) :- !.
  56. rewrite_args(N,Old,Mid) :- 
  57.         arg(N,Old,OldArg),
  58.         arg(N,Mid,MidArg),
  59.         rewrite(OldArg,MidArg),
  60.         N1 is N-1,
  61.         rewrite_args(N1,Old,Mid).
  62.  
  63. truep(t,_) :- !.
  64. truep(Wff,Tlist) :- member(Wff,Tlist).
  65.  
  66. falsep(f,_) :- !.
  67. falsep(Wff,Flist) :- member(Wff,Flist).
  68.  
  69. member(X,[X|_]) :- !.
  70. member(X,[_|T]) :- member(X,T).
  71.  
  72.  
  73. equal(  and(P,Q),
  74.         if(P,if(Q,t,f),f)
  75.         ).
  76. equal(  append(append(X,Y),Z),
  77.         append(X,append(Y,Z))
  78.         ).
  79. equal(  assignment(X,append(A,B)),
  80.         if(assignedp(X,A),
  81.            assignment(X,A),
  82.            assignment(X,B))
  83.         ).
  84. equal(  assume_false(Var,Alist),
  85.         cons(cons(Var,f),Alist)
  86.         ).
  87. equal(  assume_true(Var,Alist),
  88.         cons(cons(Var,t),Alist)
  89.         ).
  90. equal(  boolean(X),
  91.         or(equal(X,t),equal(X,f))
  92.         ).
  93. equal(  car(gopher(X)),
  94.         if(listp(X),
  95.         car(flatten(X)),
  96.         zero)
  97.         ).
  98. equal(  compile(Form),
  99.         reverse(codegen(optimize(Form),[]))
  100.         ).
  101. equal(  count_list(Z,sort_lp(X,Y)),
  102.         plus(count_list(Z,X),
  103.              count_list(Z,Y))
  104.         ).
  105. equal(  countps_(L,Pred),
  106.         countps_loop(L,Pred,zero)
  107.         ).
  108. equal(  difference(A,B),
  109.         C
  110.         ) :- difference(A,B,C).
  111. equal(  divides(X,Y),
  112.         zerop(remainder(Y,X))
  113.         ).
  114. equal(  dsort(X),
  115.         sort2(X)
  116.         ).
  117. equal(  eqp(X,Y),
  118.         equal(fix(X),fix(Y))
  119.         ).
  120. equal(  equal(A,B),
  121.         C
  122.         ) :- eq(A,B,C).
  123. equal(  even1(X),
  124.         if(zerop(X),t,odd(decr(X)))
  125.         ).
  126. equal(  exec(append(X,Y),Pds,Envrn),
  127.         exec(Y,exec(X,Pds,Envrn),Envrn)
  128.         ).
  129. equal(  exp(A,B),
  130.         C
  131.         ) :- exp(A,B,C).
  132. equal(  fact_(I),
  133.         fact_loop(I,1)
  134.         ).
  135. equal(  falsify(X),
  136.         falsify1(normalize(X),[])
  137.         ).
  138. equal(  fix(X),
  139.         if(numberp(X),X,zero)
  140.         ).
  141. equal(  flatten(cdr(gopher(X))),
  142.         if(listp(X),
  143.            cdr(flatten(X)),
  144.            cons(zero,[]))
  145.         ).
  146. equal(  gcd(A,B),
  147.         C
  148.         ) :- gcd(A,B,C).
  149. equal(  get(J,set(I,Val,Mem)),
  150.         if(eqp(J,I),Val,get(J,Mem))
  151.         ).
  152. equal(  greatereqp(X,Y),
  153.         not(lessp(X,Y))
  154.         ).
  155. equal(  greatereqpr(X,Y),
  156.         not(lessp(X,Y))
  157.         ).
  158. equal(  greaterp(X,Y),
  159.         lessp(Y,X)
  160.         ).
  161. equal(  if(if(A,B,C),D,E),
  162.         if(A,if(B,D,E),if(C,D,E))
  163.         ).
  164. equal(  iff(X,Y),
  165.         and(implies(X,Y),implies(Y,X))
  166.         ).
  167. equal(  implies(P,Q),
  168.         if(P,if(Q,t,f),t)
  169.         ).
  170. equal(  last(append(A,B)),
  171.         if(listp(B),
  172.            last(B),
  173.            if(listp(A),
  174.               cons(car(last(A))),
  175.               B))
  176.         ).
  177. equal(  length(A),
  178.         B
  179.         ) :- mylength(A,B).
  180. equal(        lesseqp(X,Y),
  181.         not(lessp(Y,X))
  182.         ).
  183. equal(  lessp(A,B),
  184.         C
  185.         ) :- lessp(A,B,C).
  186. equal(  listp(gopher(X)),
  187.         listp(X)
  188.         ).
  189. equal(  mc_flatten(X,Y),
  190.         append(flatten(X),Y)
  191.         ).
  192. equal(  meaning(A,B),
  193.         C
  194.         ) :- meaning(A,B,C).
  195. equal(  member(A,B),
  196.         C
  197.         ) :- mymember(A,B,C).
  198. equal(  not(P),
  199.         if(P,f,t)
  200.         ).
  201. equal(  nth(A,B),
  202.         C
  203.         ) :- nth(A,B,C).
  204. equal(  numberp(greatest_factor(X,Y)),
  205.         not(and(or(zerop(Y),equal(Y,1)),
  206.                 not(numberp(X))))            
  207.         ).
  208. equal(  or(P,Q),
  209.         if(P,t,if(Q,t,f),f)
  210.         ).
  211. equal(  plus(A,B),
  212.         C
  213.         ) :- plus(A,B,C).
  214. equal(  power_eval(A,B),
  215.         C
  216.         ) :- power_eval(A,B,C).
  217. equal(  prime(X),
  218.         and(not(zerop(X)),
  219.             and(not(equal(X,add1(zero))),
  220.                 prime1(X,decr(X))))
  221.         ).
  222. equal(  prime_list(append(X,Y)),
  223.         and(prime_list(X),prime_list(Y))
  224.         ).
  225. equal(  quotient(A,B),
  226.         C
  227.         ) :- quotient(A,B,C).
  228. equal(  remainder(A,B),
  229.         C
  230.         ) :- remainder(A,B,C).
  231. equal(  reverse_(X),
  232.         reverse_loop(X,[])
  233.         ).
  234. equal(  reverse(append(A,B)),
  235.         append(reverse(B),reverse(A))
  236.         ).
  237. equal(  reverse_loop(A,B),
  238.         C
  239.         ) :- reverse_loop(A,B,C).
  240. equal(  samefringe(X,Y),
  241.         equal(flatten(X),flatten(Y))
  242.         ).
  243. equal(  sigma(zero,I),
  244.         quotient(times(I,add1(I)),2)
  245.         ).
  246. equal(  sort2(delete(X,L)),
  247.         delete(X,sort2(L))
  248.         ).
  249. equal(  tautology_checker(X),
  250.         tautologyp(normalize(X),[])
  251.         ).
  252. equal(  times(A,B),
  253.         C
  254.         ) :- times(A,B,C).
  255. equal(  times_list(append(X,Y)),
  256.         times(times_list(X),times_list(Y))
  257.         ).
  258. equal(  value(normalize(X),A),
  259.         value(X,A)
  260.         ).
  261. equal(  zerop(X),
  262.         or(equal(X,zero),not(numberp(X)))
  263.         ).
  264.  
  265. difference(X, X, zero) :- !.
  266. difference(plus(X,Y), X, fix(Y)) :- !.
  267. difference(plus(Y,X), X, fix(Y)) :- !.
  268. difference(plus(X,Y), plus(X,Z), difference(Y,Z)) :- !.
  269. difference(plus(B,plus(A,C)), A, plus(B,C)) :- !.
  270. difference(add1(plus(Y,Z)), Z, add1(Y)) :- !.
  271. difference(add1(add1(X)), 2, fix(X)).
  272.  
  273. eq(plus(A,B), zero, and(zerop(A),zerop(B))) :- !.
  274. eq(plus(A,B), plus(A,C), equal(fix(B),fix(C))) :- !.
  275. eq(zero, difference(X,Y),not(lessp(Y,X))) :- !.
  276. eq(X, difference(X,Y),and(numberp(X),
  277.                           and(or(equal(X,zero),
  278.                                  zerop(Y))))) :- !.
  279. eq(times(X,Y), zero, or(zerop(X),zerop(Y))) :- !.
  280. eq(append(A,B), append(A,C), equal(B,C)) :- !.
  281. eq(flatten(X), cons(Y,[]), and(nlistp(X),equal(X,Y))) :- !.
  282. eq(greatest_factor(X,Y),zero, and(or(zerop(Y),equal(Y,1)),
  283.                                      equal(X,zero))) :- !.
  284. eq(greatest_factor(X,_),1, equal(X,1)) :- !.
  285. eq(Z, times(W,Z), and(numberp(Z),
  286.                       or(equal(Z,zero),
  287.                          equal(W,1)))) :- !.
  288. eq(X, times(X,Y), or(equal(X,zero),
  289.                      and(numberp(X),equal(Y,1)))) :- !.
  290. eq(times(A,B), 1, and(not(equal(A,zero)),
  291.                       and(not(equal(B,zero)),
  292.                           and(numberp(A),
  293.                               and(numberp(B),
  294.                                   and(equal(decr(A),zero),
  295.                                       equal(decr(B),zero))))))) :- !.
  296. eq(difference(X,Y), difference(Z,Y),if(lessp(X,Y),
  297.                                        not(lessp(Y,Z)),
  298.                                        if(lessp(Z,Y),
  299.                                           not(lessp(Y,X)),
  300.                                           equal(fix(X),fix(Z))))) :- !.
  301. eq(lessp(X,Y), Z, if(lessp(X,Y),
  302.                      equal(t,Z),
  303.                      equal(f,Z))).
  304.  
  305. exp(I, plus(J,K), times(exp(I,J),exp(I,K))) :- !.
  306. exp(I, times(J,K), exp(exp(I,J),K)).
  307.  
  308. gcd(X, Y, gcd(Y,X)) :- !.
  309. gcd(times(X,Z), times(Y,Z), times(Z,gcd(X,Y))).
  310.  
  311. mylength(reverse(X),length(X)).
  312. mylength(cons(_,cons(_,cons(_,cons(_,cons(_,cons(_,X7)))))),
  313.          plus(6,length(X7))).
  314.  
  315. lessp(remainder(_,Y), Y, not(zerop(Y))) :- !.
  316. lessp(quotient(I,J), I, and(not(zerop(I)),
  317.                             or(zerop(J),
  318.                                not(equal(J,1))))) :- !.
  319. lessp(remainder(X,Y), X, and(not(zerop(Y)),
  320.                              and(not(zerop(X)),
  321.                                  not(lessp(X,Y))))) :- !.
  322. lessp(plus(X,Y), plus(X,Z), lessp(Y,Z)) :- !.
  323. lessp(times(X,Z), times(Y,Z), and(not(zerop(Z)),
  324.                                   lessp(X,Y))) :- !.
  325. lessp(Y, plus(X,Y), not(zerop(X))) :- !.
  326. lessp(length(delete(X,L)), length(L), member(X,L)).
  327.  
  328. meaning(plus_tree(append(X,Y)),A,
  329.         plus(meaning(plus_tree(X),A),
  330.              meaning(plus_tree(Y),A))) :- !.
  331. meaning(plus_tree(plus_fringe(X)),A,
  332.         fix(meaning(X,A))) :- !.
  333. meaning(plus_tree(delete(X,Y)),A,
  334.         if(member(X,Y),
  335.            difference(meaning(plus_tree(Y),A),
  336.                       meaning(X,A)),
  337.            meaning(plus_tree(Y),A))).
  338.  
  339. mymember(X,append(A,B),or(member(X,A),member(X,B))) :- !.
  340. mymember(X,reverse(Y),member(X,Y)) :- !.
  341. mymember(A,intersect(B,C),and(member(A,B),member(A,C))).
  342.  
  343. nth(zero,_,zero).
  344. nth([],I,if(zerop(I),[],zero)).
  345. nth(append(A,B),I,append(nth(A,I),nth(B,difference(I,length(A))))).
  346.  
  347. plus(plus(X,Y),Z,
  348.      plus(X,plus(Y,Z))) :- !.
  349. plus(remainder(X,Y),
  350.      times(Y,quotient(X,Y)),
  351.      fix(X)) :- !.
  352. plus(X,add1(Y),
  353.      if(numberp(Y),
  354.         add1(plus(X,Y)),
  355.         add1(X))).
  356.  
  357. power_eval(big_plus1(L,I,Base),Base,
  358.            plus(power_eval(L,Base),I)) :- !.
  359. power_eval(power_rep(I,Base),Base,
  360.            fix(I)) :- !.
  361. power_eval(big_plus(X,Y,I,Base),Base,
  362.            plus(I,plus(power_eval(X,Base),
  363.                        power_eval(Y,Base)))) :- !.
  364. power_eval(big_plus(power_rep(I,Base),
  365.                     power_rep(J,Base),
  366.                     zero,
  367.                     Base),
  368.            Base,
  369.            plus(I,J)).
  370.  
  371. quotient(plus(X,plus(X,Y)),2,plus(X,quotient(Y,2))).
  372. quotient(times(Y,X),Y,if(zerop(Y),zero,fix(X))).
  373.  
  374. remainder(_,         1,zero) :- !.
  375. remainder(X,         X,zero) :- !.
  376. remainder(times(_,Z),Z,zero) :- !.
  377. remainder(times(Y,_),Y,zero).
  378.  
  379. reverse_loop(X,Y,  append(reverse(X),Y)) :- !.
  380. reverse_loop(X,[], reverse(X)          ).
  381.  
  382. times(X,         plus(Y,Z),      plus(times(X,Y),times(X,Z))      ) :- !.
  383. times(times(X,Y),Z,              times(X,times(Y,Z))              ) :- !.
  384. times(X,         difference(C,W),difference(times(C,X),times(W,X))) :- !.
  385. times(X,         add1(Y),        if(numberp(Y),
  386.                                     plus(X,times(X,Y)),
  387.                                     fix(X))                       ).
  388.